package org.stragma.apply.modules

import org.kiama.rewriting._
import org.kiama.rewriting.Rewriter.{id,innermost,not,rulefs,Strategy,Term,where}

import org.stragma.apply.modules.Normalise._
import org.stragma.apply.signatures.Apply._

import org.stragma.apply.util.LogicalOperators._
import org.stragma.apply.util.Math._

object Beautify {
	
	/*
	 * Port of main strategy
	 * beautify = innermost(NegMulConst); innermost(SortNeg); innermost(Beautify <+ LeftGroup <+ EvalAdd0 <+ EvalNeg <+ RemoveMul1); innermost(NegMul)
	 */
	def beautify1 =
		// Scala does not like it when names are re-used so we have renamed the primary strategy beautify1
		innermost(NegMulConst) <* 
		innermost(SortNeg) <* 
		innermost(Beautify <+ LeftGroup <+ EvalAdd0 <+ EvalNeg <+ RemoveMul1) <* 
		innermost(NegMul)
	
	// The strategies all-neg and negate-all were not ported as they are not used
	
	/*
	 * Port of NegMulConst Strategy
	 */
	def NegMulConst = rulefs {
		// If term is negated, negate product (leading to subtraction later on)
 		// NegMulConst : |[ -e * i ]|      -> |[ -(e * i) ]|
		// NegMulConst : |[ e * i ]|       -> |[ -(e * j) ]|         where <ltS>(i,"0"); <subtS>("0",i) => j
		// NegMulConst : |[ -e ]|          -> |[ -(e * 1) ]|         where <not(?Mul(_,Int(_)))>e ; <not(?Int(_))>e
		case Mul(Neg(e),i : Int) => Neg(Mul(e,i))
		case Mul(e,i : Int) if (ltS(i,Int("0")).isDefined) => Neg(Mul(e,subtS(Int("0"),i)))
		case Neg(e) if (notMulIntExprGuard(e) && notIntExprGuard(e)) => Neg(Mul(e,Int("1")))
	}

	/*
	 * Port of SortNeg Strategy
	 */
	def SortNeg = rulefs {
		// Sort negative leading terms after positive (otherwise, minimal reordering)
		// SortNeg : |[ -e1 + e2 ]|        -> |[ e2 + -e1 ]|       where <not(?Neg(_))>e2 ; <not(?Int(_))>e2
		// SortNeg : |[ e + -e1 + e2 ]|    -> |[ e + e2 + -e1 ]|   where <not(?Neg(_))>e2 ; <not(?Int(_))>e2
		case Add(Neg(e1),e2) if (notNegExprGuard(e2) && notIntExprGuard(e2)) => Add(e2,Neg(e1))
		case Add(Add(e,Neg(e1)),e2) if (notNegExprGuard(e2) && notIntExprGuard(e2)) => Add(Add(e,e2),Neg(e1))

		// Sort multipliers that are negative but greater than 1 ahead of 1
		// SortNeg : |[ -(e1 * 1) + -(e2 * i) ]| -> |[ -(e2 * i) + -(e1 * 1) ]|  where <gtS>(i,"1")
		// SortNeg : |[ e + -(e1 * 1) + -(e2 * i) ]| -> |[ e + -(e2 * i) + -(e1 * 1) ]|  where <gtS>(i,"1")
		case Add(Neg(Mul(e1,Int("1"))),Neg(Mul(e2,i : Int))) if (gtS(i,Int("1")).isDefined)
			=> Add(Neg(Mul(e2,i : Int)),Neg(Mul(e1,Int("1"))))
		case Add(Add(e,Neg(Mul(e1,Int("1")))),Neg(Mul(e2,i : Int))) if (gtS(i,Int("1")).isDefined)
			=> Add(Add(e,Neg(Mul(e2,i))),Neg(Mul(e1,Int("1")))) 
	}

	/*
	 * Port of Strategy Beautify
	 */
	def Beautify = rulefs {
		// Negation becomes subtraction
 		// Beautify : |[ e1 + -e2 ]|       -> |[ e1 - e2 ]|
		case Add(e1,Neg(e2)) => Sub(e1,e2)

		// Multiplier constants move before the expressions they multiply
 		// Beautify : |[ e * i ]|          -> |[ i * e ]|          where <not(?Int(_))>e
		case Mul(e,i : Int) if (notIntExprGuard(e)) => Mul(i,e)

 		// Negative added constant becomes subtraction
 		// Beautify : |[ e + i ]|          -> |[ e - j ]|          where <ltS>(i,"0") ; <subtS>("0",i) => j
		case Add(e,i : Int) if (ltS(i,Int("0")).isDefined) => Sub(e,subtS(Int("0"),i))
		
		// Move subtracted terms to right-hand side of comparison
 		// Beautify : |[ e1 - e2 > e ]|    -> |[ e1 > e2 + e ]|
 		// Beautify : |[ e1 - e2 >= e ]|   -> |[ e1 >= e2 + e ]|
 		// Beautify : |[ e1 - e2 = e ]|    -> |[ e1 = e2 + e ]|
		// Beautify : |[ e1 - e2 < e ]|    -> |[ e1 < e2 + e ]|
 		// Beautify : |[ e1 - e2 <= e ]|   -> |[ e1 <= e2 + e ]|
 		// Beautify : |[ e1 - e2 != e ]|   -> |[ e1 != e2 + e ]|
		case Gt(Sub(e1,e2),e) => Gt(e1,Add(e2,e))
		case Geq(Sub(e1,e2),e) => Geq(e1,Add(e2,e))
		case Equ(Sub(e1,e2),e) => Equ(e1,Add(e2,e))
		case Lt(Sub(e1,e2),e) => Lt(e1,Add(e2,e))
		case Leq(Sub(e1,e2),e) => Leq(e1,Add(e2,e))
		case Neq(Sub(e1,e2),e) => Neq(e1,Add(e2,e))
	}

	private val notMulIntExprGuard = (e:TExp) => {
		where(not(rulefs { case Mul(_,Int(_)) => id }))(e).isDefined
	}

	/*
	 * Used by the Beautify rules as part of a conditional guard
	 */
	private val notNegExprGuard = (e:TExp) => { 
		where(not(rulefs { case Neg(_) => id }))(e).isDefined 	// isDefined is used to convert the Option result into a Boolean
	}

	/*
	 * Used by the Beautify rules as part of a conditional guard
	 */
	private val notIntExprGuard = (e:TExp) => { 
		where(not(rulefs { case Int(_) => id }))(e).isDefined 	// isDefined is used to convert the Option result into a Boolean
	}

	/*
	 * Port of Strategy NegMul
	 */
	def NegMul = rulefs {
		// NegMul : |[ -(i * e) ]|         -> |[ j * e ]|          where <subtS>("0",i) => j
		case Neg(Mul(i : Int,e)) => Mul(subtS(Int("0"),i),e)
	}

	/*
	 * Port of Strategy RemoveMul1
	 */
	def RemoveMul1 = rulefs {
		// RemoveMul1 : |[ 1 * e ]|        -> |[ e ]|
 		// RemoveMul1 : |[ -1 * e ]|       -> |[ -e ]|
		case Mul(Int("1"),e) => e
		case Mul(Int("-1"),e) => Neg(e)
	}
	
	/*
	 * Helper method to invoke function from Java
	 */
	def beautifyHelper(term : Term) : Term = (beautify1(term)).get
	
	/*
	 * This helper method executes applyDesugar n times and returns
	 * the very last result the caller
	 */
	def beautifyHelper(term : Term, n : scala.Int) : Term = {
		var result : Term = scala.None
		for(i <- 0 until n) {
			result = (beautify1(term)).get
			
			// Added the println to mimic the way strategoxt.jar works
			println(result)
		}
		
		result
	}
	
	/*
	 * This helper method executes applyDesugar n times and returns
	 * the very last result to the caller
	 */
	def beautifyHelper(file : String, n : scala.Int) : Term = {
		val iTerm = loadTermFromFile(file)
		beautifyHelper(iTerm, n)
	}
}